Nuprl Lemma : strong-subtype-l_member-type
0,22
postcript
pdf
A
,
B
:Type. strong-subtype(
A
;
B
)
(
L
:
A
List,
x
:
B
. (
x
L
)
x
A
)
latex
Definitions
l
[
i
]
,
,
A
B
,
A
,
False
,
||
as
||
,
Prop
,
x
:
A
.
B
(
x
)
,
S
T
,
P
Q
,
(
x
l
)
,
strong-subtype(
A
;
B
)
,
A
&
B
,
x
:
A
.
B
(
x
)
,
t
T
Lemmas
strong-subtype
wf
,
l
member
wf
,
select
wf
origin
A, B:Type. strong-subtype(A;B) 
(L:A List, x:B. (x 
L) x A) A, B:Type. strong-subtype(A;B) (L:A List, x:B. (x L) x A) 
B
A
x:A. B(x)
T Q l)x:A. B(x) T